| Definitions | Type, t  T, ||as||, a < b, P   Q, False,  A, P & Q, A  B, i j < k,  , {x:A| B(x)} , {i..j }, Void, x:A  B(x),  x:A. B(x),  , (x l), #$n, r s,   x. t(x), xL. P(x), l[i],  a j < b. E(j), s = t, x:A  B(x), type List, Id, FinProbSpace, IdLnk,  , State(ds), a:A fp B(a), Outcome, f(a),  b, Normal(ds), xdom(f). v=f(x) P(x;v), rec(x.A(x)), DeclaredType(ds;x), Realizer, Atom$n, Top,  ,  b,  , P  Q, Unit, left + right, if b then t else f fi , IdDeq, "$x", [car / cdr], [], x : v, x.A(x),  x:A.B(x), f(x)?z, <a, b>, True, es realizer ind Rsframe compseq tag def, R-Feasible(R), inr x , Rsframe(lnk;tag;L), Normal(T), A c B, isrcv_locl{isrcv_locl_compseq_tag_def:ObjectId}(a), es realizer ind Rsends compseq tag def, Rsends(ds;knd;T;l;dt;g), es realizer ind Rpre compseq tag def, Rpre(loc;ds;a;p;P), Knd, hd(l), i <z j, i z j, tl(l), {T}, SQType(T), s ~ t, P  Q, Dec(P),  x:A. B(x), Rinit-v(x1), Rinit-x(x1), Rinit?(x1), Reffect-f(x1), Reffect-x(x1), Reffect?(x1), Rinit-discrete(A), Reffect-discrete(A), R-discrete_compat(A;B), locl(a), P Q, lnk-decl(l;dt), f  g, KindDeq, f || g, a = b, (i = j), Rsends-T(x1), Rsends-dt(x1), Rsends-l(x1), Rsends-knd(x1), Rsends?(x1), Reffect-T(x1), Reffect-knd(x1), Rrframe-L(x1), Rpre-a(x1), Rpre-ds(x1), Rrframe-x(x1), Rrframe?(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-g(x1), Rsframe-tag(x1), Rsframe-lnk(x1), Rsframe?(x1), Reffect-ds(x1), Raframe-L(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Rframe-x(x1), Rframe?(x1), Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), R-interface-compat(A;B), R-frame-compat(A;B), p = q, R-base-domain(R), Rda(R), Rds(R), R-loc(R), A || B, (x,yL. P(x;y)), source(l), weakPrecondSendR2{$a:ut2, $tg:ut2}(T; t; p; l; ds; P; f) |
| Lemmas | R-feasible-Rlist, lsrc wf, es realizer wf, locl wf, Rsframe wf, fpf-cap wf, fpf-compatible-join, fpf-compatible-self, fpf-compatible-symmetry, lnk-decl-compatible-single, R-compat-disjoint, R-compat-symmetry, not functionality wrt iff, assert-eq-id, eq id wf, Id sq, fpf-empty-compatible-right, Kind-deq wf, fpf-join wf, top wf, fpf-trivial-subtype-top, lnk-decl wf, assert-eq-lnk, select member, R-Feasible wf, decidable int equal, Rpre wf, Rsends wf, unit wf, fpf wf, Knd wf, IdLnk wf, finite-prob-space wf, false wf, natural number wf p-outcome, normal-ds-single, fpf-single wf, decl-type wf, id-deq wf, ifthenelse wf, fpf-cap-single1, fpf-cap-single, eqof eq btrue, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, le wf, length wf nat, nat wf, normal-ds wf, assert wf, p-outcome wf, decl-state wf, bool wf, Id wf, rationals wf, qsum wf, length wf1, select wf, int seg wf, l all wf2, qle wf, int inc rationals, l member wf |
f:({s:State(ds)|